msystem\{i:l\} $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{$M$:Id$\rightarrow$msga\{i:l\}$\mid$ $\forall$${\it loc}$:Id. ma{-}feasible\{i:l\}(($M$(${\it loc}$)))\}